ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da). eclcatch?(x)   

latex

Definitions	x. t(x), x,y,z. t(x;y;z), x,y,z,w. t(x;y;z;w), x,y. t(x;y), eclcatch?(x), t  T, x:A. B(x), x(s), x(s1,s2,s3), x(s1,s2,s3,s4), x(s1,s2)
Lemmas	Id wf, Knd wf, fpf wf, ecl wf, btrue wf, nat wf, ma-valtype wf, decl-state wf, bfalse wf, bool wf, ecl ind wf